Search Results

Documents authored by Li, Yao

Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2022.27
Improving Pedestrians Traffic Priority via Grouping and Virtual Lanes in Shared Spaces (Short Paper)

Authors: Yao Li, Vinu Kamalasanan, Mariana Batista, and Monika Sester

Published in: LIPIcs, Volume 240, 15th International Conference on Spatial Information Theory (COSIT 2022)

Abstract
The shared space design is applied in urban streets to support barrier-free movement and integrate traffic participants (such as pedestrians, cyclists and vehicles) into a common road space. Regardless of the low-speed environment, sharing space with motor vehicles can make vulnerable road users feel uneasy. Yet, walking in groups increases their confidence as well as influence the yielding behavior of drivers. Therefore, we propose an innovative approach to support the crossing of pedestrians via grouping and project the virtual lanes in shared spaces. This paper presents the important components of the crowd steering system, discusses the enablers and gaps in the current approach, and illustrates the proposed idea with concept diagrams.
Cite as

Yao Li, Vinu Kamalasanan, Mariana Batista, and Monika Sester. Improving Pedestrians Traffic Priority via Grouping and Virtual Lanes in Shared Spaces (Short Paper). In 15th International Conference on Spatial Information Theory (COSIT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 240, pp. 27:1-27:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.COSIT.2022.27,
  author =	{Li, Yao and Kamalasanan, Vinu and Batista, Mariana and Sester, Monika},
  title =	{{Improving Pedestrians Traffic Priority via Grouping and Virtual Lanes in Shared Spaces}},
  booktitle =	{15th International Conference on Spatial Information Theory (COSIT 2022)},
  pages =	{27:1--27:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-257-0},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{240},
  editor =	{Ishikawa, Toru and Fabrikant, Sara Irina and Winter, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2022.27},
  URN =		{urn:nbn:de:0030-drops-169125},
  doi =		{10.4230/LIPIcs.COSIT.2022.27},
  annote =	{Keywords: shared space, urban traffic system, augmented reality, pedestrian grouping}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.32
Verifying an HTTP Key-Value Server with Interaction Trees and VST

Authors: Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.
Cite as

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ITP.2021.32,
  author =	{Zhang, Hengchu and Honor\'{e}, Wolf and Koh, Nicolas and Li, Yao and Li, Yishuai and Xia, Li-Yao and Beringer, Lennart and Mansky, William and Pierce, Benjamin and Zdancewic, Steve},
  title =	{{Verifying an HTTP Key-Value Server with Interaction Trees and VST}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.32},
  URN =		{urn:nbn:de:0030-drops-139273},
  doi =		{10.4230/LIPIcs.ITP.2021.32},
  annote =	{Keywords: formal verification, Coq, HTTP, deep specification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact